
1.
msc diagrams: CW_teardown1(20) and call_setup_failure2(9)
INCONSISTENCY:
Matching formula: m20 = m9
Precondition 1: rel (k20 , n20 , cw hold connect m20);
Precondition 2: state (m9 , ringing n9);
Post condition 1: rel (k20 , n20 , connected);
Post condition 2: state (n9 , idle);
2.
msc diagrams: CW_teardown1(20) and call_teardown(5)
INCONSISTENCY:
Matching formula: m20 = m5
Precondition 1: rel (k20 , n20 , cw hold connect m20);
Precondition 2: rel (m5 , n5 , connected);
Post condition 1: rel (k20 , n20 , connected);
Post condition 2: state (n5 , dial);
3.
msc diagrams: CW_teardown2(18) and call_setup_failure2(9)
INCONSISTENCY:
Matching formula: m18 = m9
Precondition 1: rel (k18 , m18 , cw hold connect n18);
Precondition 2: state (m9 , ringing n9);
Post condition 1: rel (k18 , n18 , cw hold);
Post condition 2: state (n9 , idle);
4.
msc diagrams: CW_teardown2(18) and call_teardown(5)
INCONSISTENCY:
Matching formula: m18 = m5
Precondition 1: rel (k18 , m18 , cw hold connect n18);
Precondition 2: rel (m5 , n5 , connected);
Post condition 1: rel (k18 , n18 , cw hold);
Post condition 2: state (n5 , dial);


5.
msc diagrams: CW_teardown3(15) and call_setup_failure2(9)
INCONSISTENCY:
Matching formula: k15 = m9
Precondition 1: rel (k15 , n15 , cw hold connect m15);
Precondition 2: state (m9 , ringing n9);
Post condition 1: state (m15 , dial) & state (n15 , dial);
Post condition 2: state (n9 , idle);
6.
msc diagrams: CW_teardown3(15) and call_teardown(5)
INCONSISTENCY:
Matching formula: k15 = m5
Precondition 1: rel (k15 , n15 , cw hold connect m15);
Precondition 2: rel (m5 , n5 , connected);
Post condition 1: state (m15 , dial) & state (n15 , dial);
Post condition 2: state (n5 , dial);
